Issue543a.agda:36,50-54
true != (unsquash (squash _)) of type Bool
when checking that the expression refl has type
true ≡ unsquash (squash _)
